<!DOCTYPE html>
<html class="writer-html5" lang="en" >
<head>
  <meta charset="utf-8" /><meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />

  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>3. Parity and divisibility &mdash; The Mechanics of Proof, by Heather Macbeth</title>
      <link rel="stylesheet" href="_static/pygments.css" type="text/css" />
      <link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
      <link rel="stylesheet" href="_static/css/custom.css" type="text/css" />
    <link rel="shortcut icon" href="_static/favicon.ico"/>
  <!--[if lt IE 9]>
    <script src="_static/js/html5shiv.min.js"></script>
  <![endif]-->
  
        <script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
        <script src="_static/jquery.js"></script>
        <script src="_static/underscore.js"></script>
        <script src="_static/doctools.js"></script>
        <script async="async" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="genindex.html" />
    <link rel="search" title="Search" href="search.html" />
    <link rel="next" title="4. Proofs with structure, II" href="04_Proofs_with_Structure_II.html" />
    <link rel="prev" title="2. Proofs with structure" href="02_Proofs_with_Structure.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >
            <a href="index.html" class="icon icon-home"> The Mechanics of Proof
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul>
<li class="toctree-l1"><a class="reference internal" href="00_Introduction.html">Preface</a></li>
</ul>
<ul class="current">
<li class="toctree-l1"><a class="reference internal" href="01_Proofs_by_Calculation.html">1. Proofs by calculation</a></li>
<li class="toctree-l1"><a class="reference internal" href="02_Proofs_with_Structure.html">2. Proofs with structure</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">3. Parity and divisibility</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#definitions-parity">3.1. Definitions; parity</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#example">3.1.1. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id2">3.1.2. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#odd-hyp-goal">3.1.3. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id4">3.1.4. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#typical-parity">3.1.5. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id6">3.1.6. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#even">3.1.7. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id8">3.1.8. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#even-or-odd">3.1.9. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#exercises">3.1.10. Exercises</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#divisibility">3.2. Divisibility</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#id13">3.2.1. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id14">3.2.2. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id15">3.2.3. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id16">3.2.4. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id17">3.2.5. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#not-divisible">3.2.6. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#dvd-bd-1">3.2.7. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#dvd-bd-2">3.2.8. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id21">3.2.9. Exercises</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#modular-arithmetic-theory">3.3. Modular arithmetic: theory</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#id22">3.3.1. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id23">3.3.2. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#modeq-add">3.3.3. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#exercise">3.3.4. Exercise</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id25">3.3.5. Exercise</a></li>
<li class="toctree-l3"><a class="reference internal" href="#modeq-mul">3.3.6. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#no-mod-division">3.3.7. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id28">3.3.8. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#modeq-pow">3.3.9. Exercise</a></li>
<li class="toctree-l3"><a class="reference internal" href="#modeq-refl">3.3.10. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#apply-mod-lemmas-example">3.3.11. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id32">3.3.12. Exercises</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#modular-arithmetic-calculations">3.4. Modular arithmetic: calculations</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#id33">3.4.1. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id34">3.4.2. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id35">3.4.3. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#first-mod-cases">3.4.4. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id37">3.4.5. Exercises</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#bezout-s-identity">3.5. B&#233;zout&#8217;s identity</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#bezout-prob1">3.5.1. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#bezout-prob2">3.5.2. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#bezout-prob3">3.5.3. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id41">3.5.4. Exercises</a></li>
</ul>
</li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="04_Proofs_with_Structure_II.html">4. Proofs with structure, II</a></li>
<li class="toctree-l1"><a class="reference internal" href="05_Logic.html">5. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="06_Induction.html">6. Induction</a></li>
<li class="toctree-l1"><a class="reference internal" href="07_Number_Theory.html">7. Number theory</a></li>
<li class="toctree-l1"><a class="reference internal" href="08_Functions.html">8. Functions</a></li>
<li class="toctree-l1"><a class="reference internal" href="09_Sets.html">9. Sets</a></li>
<li class="toctree-l1"><a class="reference internal" href="10_Relations.html">10. Relations</a></li>
</ul>
<ul>
<li class="toctree-l1"><a class="reference internal" href="Index_of_Tactics.html">Index of Lean tactics</a></li>
<li class="toctree-l1"><a class="reference internal" href="Mainstream_Lean.html">Transitioning to mainstream Lean</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="index.html">The Mechanics of Proof</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="index.html" class="icon icon-home"></a> &raquo;</li>
      <li><span class="section-number">3. </span>Parity and divisibility</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/03_Parity_and_Divisibility.rst.txt" rel="nofollow"> View page source</a>
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             
  <section id="parity-and-divisibility">
<span id="id1"></span><h1><span class="section-number">3. </span>Parity and divisibility<a class="headerlink" href="#parity-and-divisibility" title="Permalink to this headline">&#61633;</a></h1>
<p>The problems in this chapter concern some elementary properties of natural numbers
and integers: <em>parity</em> (whether a number is <em>even</em> or <em>odd</em>), <em>divisibility</em>, and
<em>congruence modulo</em> <span class="math notranslate nohighlight">\(n\)</span>.</p>
<p>There are no new logical symbols like <span class="math notranslate nohighlight">\(\lor\)</span> or <span class="math notranslate nohighlight">\(\exists\)</span> in this
chapter, and no major additions (such as the use of intermediate steps or lemmas)
to our reasoning toolkit.  Thus this chapter functions as a breather between the
hard work of <a class="reference internal" href="02_Proofs_with_Structure.html#proofs-with-structure"><span class="std std-numref">Chapter 2</span></a> and
<a class="reference internal" href="04_Proofs_with_Structure_II.html#proofs-with-structure-ii"><span class="std std-numref">Chapter 4</span></a>, a chance to consolidate what you
have learned.</p>
<section id="definitions-parity">
<span id="parity"></span><h2><span class="section-number">3.1. </span>Definitions; parity<a class="headerlink" href="#definitions-parity" title="Permalink to this headline">&#61633;</a></h2>
<section id="example">
<span id="odd"></span><h3><span class="section-number">3.1.1. </span>Example<a class="headerlink" href="#example" title="Permalink to this headline">&#61633;</a></h3>
<p>When a mathematical term is introduced for the first time, it is given a definition.</p>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>An integer <span class="math notranslate nohighlight">\(a\)</span> is <em>odd</em>, if there exists an integer <span class="math notranslate nohighlight">\(k\)</span>, such that <span class="math notranslate nohighlight">\(a=2k+1\)</span>.</p>
</div>
<p>Here&#8217;s how we make a definition in Lean.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">Odd</span> <span class="o">(</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="kt">Prop</span> <span class="o">:=</span> <span class="bp">&#8707;</span> <span class="n">k</span><span class="o">,</span> <span class="n">a</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">k</span> <span class="bp">+</span> <span class="mi">1</span>
</pre></div>
</div>
<p>On paper, you need to memorize every definition; this is crucial to be able to work with them.
In Lean, when you see a term whose definition you&#8217;d like to double-check, you can right-click
(Windows) / two-finger-click (Mac) to bring up an option &#8220;Go to Definition&#8221;.  This will send you
to the place in the Lean code where the definition was introduced.  (The keyboard shortcut
<code class="docutils literal notranslate"><span class="pre">Ctrl</span></code>-<code class="docutils literal notranslate"><span class="pre">-</span></code> will bring you back from that definition to where you were working before.)</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that <span class="math notranslate nohighlight">\(7\)</span> is odd.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p><span class="math notranslate nohighlight">\(7=2\cdot 3+1\)</span>, so <span class="math notranslate nohighlight">\(7\)</span> is odd.</p>
</div>
<p>Here&#8217;s how this problem looks in Lean.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Odd</span> <span class="o">(</span><span class="mi">7</span><span class="o">:</span><span class="n">&#8484;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
<p>The goal state at the start is:</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>&#8866; Odd 7
</pre></div>
</div>
<p>You can check a definition within a proof using the <code class="docutils literal notranslate"><span class="pre">dsimp</span></code> (&#8220;definitional-simplify&#8221;) tactic.
Here, you can type <code class="docutils literal notranslate"><span class="pre">dsimp</span> <span class="pre">[Odd]</span></code> within the proof to have the definition of &#8220;odd&#8221; unfolded for
you:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Odd</span> <span class="o">(</span><span class="mi">7</span><span class="o">:</span><span class="n">&#8484;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Odd</span><span class="o">]</span>
</pre></div>
</div>
<p>After doing this, the goal is displayed using the definition of &#8220;odd&#8221; rather than with the word
&#8220;odd&#8221;:</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>&#8866; &#8707; (k : &#8484;), 7 = 2 * k + 1
</pre></div>
</div>
<p>This is optional, though; the proof will still work if you delete the <code class="docutils literal notranslate"><span class="pre">dsimp</span></code> line.</p>
<p>Here is the full Lean translation of the solution.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Odd</span> <span class="o">(</span><span class="mi">7</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Odd</span><span class="o">]</span>
  <span class="n">use</span> <span class="mi">3</span>
  <span class="n">numbers</span>
</pre></div>
</div>
<p>If you don&#8217;t quite follow the proof &#8211; either in its text version or its Lean version &#8211; then
reread some of the examples in <a class="reference internal" href="02_Proofs_with_Structure.html#exists"><span class="std std-numref">Section 2.5</span></a>, such as
<a class="reference internal" href="02_Proofs_with_Structure.html#simple-existential"><span class="std std-numref">Example 2.5.3</span></a>.</p>
</section>
<section id="id2">
<h3><span class="section-number">3.1.2. </span>Example<a class="headerlink" href="#id2" title="Permalink to this headline">&#61633;</a></h3>
<p>Here&#8217;s a similar example.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that <span class="math notranslate nohighlight">\(-3\)</span> is odd.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Odd</span> <span class="o">(</span><span class="bp">-</span><span class="mi">3</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
<p>You should show that <span class="math notranslate nohighlight">\(-3=2k+1\)</span> for some integer <span class="math notranslate nohighlight">\(k\)</span>.  But what is the <span class="math notranslate nohighlight">\(k\)</span> that
works?</p>
</section>
<section id="odd-hyp-goal">
<span id="id3"></span><h3><span class="section-number">3.1.3. </span>Example<a class="headerlink" href="#odd-hyp-goal" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Prove that if <span class="math notranslate nohighlight">\(n\)</span> is an odd integer, then <span class="math notranslate nohighlight">\(3n+2\)</span> is odd.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Let <cite>n</cite> be odd.  Then there exists an integer <span class="math notranslate nohighlight">\(k\)</span> such that <span class="math notranslate nohighlight">\(n = 2k+1\)</span>.  Thus</p>
<div class="math notranslate nohighlight">
\[\begin{split}3 n + 2 &amp;= 3 (2 k + 1) + 2 \\
&amp; = 2 (3 k + 2) + 1,\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(3n+2\)</span> is odd.</p>
</div>
<p>In the Lean version of the problem, the goal state initially looks like this.</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>n : &#8484;
hn : Odd n
&#8866; Odd (3 * n + 2)
</pre></div>
</div>
<p>If you want to unfold the definition <code class="docutils literal notranslate"><span class="pre">Odd</span></code> in the goal, you can use <code class="docutils literal notranslate"><span class="pre">dsimp</span> <span class="pre">[Odd]</span></code>, as
discussed in <a class="reference internal" href="#odd"><span class="std std-numref">Example 3.1.1</span></a>.  If you want to unfold the definition <code class="docutils literal notranslate"><span class="pre">Odd</span></code> everywhere
(goals and hypotheses), you can use <code class="docutils literal notranslate"><span class="pre">dsimp</span> <span class="pre">[Odd]</span> <span class="pre">at</span> <span class="pre">*</span></code>.  After that the goal state looks like
this:</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>n : &#8484;
hn : &#8707; (k : &#8484;), n = 2 * k + 1
&#8866; &#8707; (k : &#8484;), 3 * n + 2 = 2 * k + 1
</pre></div>
</div>
<p>This is our first encounter with something which might be confusing.  The variable inside an
existential is a &#8220;throwaway&#8221; variable, which exists only for the duration of the sentence.  So the
same variable might occur within the goal state repeatedly, without meaning the same thing.  Here
the <code class="docutils literal notranslate"><span class="pre">k</span></code> in the hypothesis <code class="docutils literal notranslate"><span class="pre">hn</span></code> is different from the <code class="docutils literal notranslate"><span class="pre">k</span></code> in the goal; it&#8217;s just the default
name when the definition &#8220;odd&#8221; is unfolded.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hn</span> <span class="o">:</span> <span class="n">Odd</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="n">Odd</span> <span class="o">(</span><span class="mi">3</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">2</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Odd</span><span class="o">]</span> <span class="n">at</span> <span class="bp">*</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">k</span><span class="o">,</span> <span class="n">hk</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hn</span>
  <span class="n">use</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">k</span> <span class="bp">+</span> <span class="mi">2</span>
  <span class="k">calc</span>
    <span class="mi">3</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">=</span> <span class="mi">3</span> <span class="bp">*</span> <span class="o">(</span><span class="mi">2</span> <span class="bp">*</span> <span class="n">k</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hk</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="o">(</span><span class="mi">3</span> <span class="bp">*</span> <span class="n">k</span> <span class="bp">+</span> <span class="mi">2</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
</pre></div>
</div>
<p>Again, you can check that the <code class="docutils literal notranslate"><span class="pre">dsimp</span></code> line is not actually needed in the solution.</p>
</section>
<section id="id4">
<h3><span class="section-number">3.1.4. </span>Example<a class="headerlink" href="#id4" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(n\)</span> be an integer. Prove that if <span class="math notranslate nohighlight">\(n\)</span> is odd, then <span class="math notranslate nohighlight">\(7n-4\)</span> is odd.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hn</span> <span class="o">:</span> <span class="n">Odd</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="n">Odd</span> <span class="o">(</span><span class="mi">7</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">-</span> <span class="mi">4</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="typical-parity">
<span id="id5"></span><h3><span class="section-number">3.1.5. </span>Example<a class="headerlink" href="#typical-parity" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Prove that if the integers <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> are odd, then <span class="math notranslate nohighlight">\(x+y+1\)</span> is odd.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Since <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> are odd, there exists an integer <span class="math notranslate nohighlight">\(a\)</span> such that
<span class="math notranslate nohighlight">\(x=2a+1\)</span>, and there exists an integer <span class="math notranslate nohighlight">\(b\)</span> such that <span class="math notranslate nohighlight">\(y=2b+1\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}x + y + 1 &amp;= (2 a + 1) + (2 b + 1) + 1 \\
&amp;= 2  (a + b + 1) + 1,\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(x+y+1\)</span> is odd.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">x</span> <span class="n">y</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hx</span> <span class="o">:</span> <span class="n">Odd</span> <span class="n">x</span><span class="o">)</span> <span class="o">(</span><span class="n">hy</span> <span class="o">:</span> <span class="n">Odd</span> <span class="n">y</span><span class="o">)</span> <span class="o">:</span> <span class="n">Odd</span> <span class="o">(</span><span class="n">x</span> <span class="bp">+</span> <span class="n">y</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">a</span><span class="o">,</span> <span class="n">ha</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hx</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">b</span><span class="o">,</span> <span class="n">hb</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hy</span>
  <span class="n">use</span> <span class="n">a</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">1</span>
  <span class="k">calc</span>
    <span class="n">x</span> <span class="bp">+</span> <span class="n">y</span> <span class="bp">+</span> <span class="mi">1</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">+</span> <span class="mi">1</span> <span class="bp">+</span> <span class="o">(</span><span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">ha</span><span class="o">,</span> <span class="n">hb</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="o">(</span><span class="n">a</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
</pre></div>
</div>
</section>
<section id="id6">
<h3><span class="section-number">3.1.6. </span>Example<a class="headerlink" href="#id6" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Prove that if the integers <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> are odd, then <span class="math notranslate nohighlight">\(xy+2y\)</span> is odd.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Since <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> are odd, there exists an integer <span class="math notranslate nohighlight">\(a\)</span> such that
<span class="math notranslate nohighlight">\(x=2a+1\)</span>, and there exists an integer <span class="math notranslate nohighlight">\(b\)</span> such that <span class="math notranslate nohighlight">\(y=2b+1\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}x y + 2 y &amp;= (2 a + 1)  (2 b + 1) + 2 (2 b + 1) \\
&amp;= 2  (2 a b + 3 b + a + 1) + 1,\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(xy+2y\)</span> is odd.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">x</span> <span class="n">y</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hx</span> <span class="o">:</span> <span class="n">Odd</span> <span class="n">x</span><span class="o">)</span> <span class="o">(</span><span class="n">hy</span> <span class="o">:</span> <span class="n">Odd</span> <span class="n">y</span><span class="o">)</span> <span class="o">:</span> <span class="n">Odd</span> <span class="o">(</span><span class="n">x</span> <span class="bp">*</span> <span class="n">y</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">y</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="even">
<span id="id7"></span><h3><span class="section-number">3.1.7. </span>Example<a class="headerlink" href="#even" title="Permalink to this headline">&#61633;</a></h3>
<p>You can probably guess the definition of &#8220;even&#8221;.</p>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>An integer <span class="math notranslate nohighlight">\(a\)</span> is <em>even</em>, if there exists an integer <span class="math notranslate nohighlight">\(k\)</span>, such that <span class="math notranslate nohighlight">\(a=2k\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">Even</span> <span class="o">(</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="kt">Prop</span> <span class="o">:=</span> <span class="bp">&#8707;</span> <span class="n">k</span><span class="o">,</span> <span class="n">a</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">k</span>
</pre></div>
</div>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(m\)</span> be an integer. Prove that if <span class="math notranslate nohighlight">\(m\)</span> is odd, then <span class="math notranslate nohighlight">\(3m-5\)</span> is even.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Since <cite>m</cite> is odd, there exists an integer <span class="math notranslate nohighlight">\(t\)</span> such that <span class="math notranslate nohighlight">\(m = 2t+1\)</span>.  Thus</p>
<div class="math notranslate nohighlight">
\[\begin{split}3 m-5 &amp;= 3 (2 t + 1) - 5 \\
&amp; = 2 (3 t - 1),\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(3m-5\)</span> is even.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">m</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hm</span> <span class="o">:</span> <span class="n">Odd</span> <span class="n">m</span><span class="o">)</span> <span class="o">:</span> <span class="n">Even</span> <span class="o">(</span><span class="mi">3</span> <span class="bp">*</span> <span class="n">m</span> <span class="bp">-</span> <span class="mi">5</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="id8">
<h3><span class="section-number">3.1.8. </span>Example<a class="headerlink" href="#id8" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(n\)</span> be an even integer. Prove that <span class="math notranslate nohighlight">\(n ^ 2 + 2 n - 5\)</span> is odd.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hn</span> <span class="o">:</span> <span class="n">Even</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="n">Odd</span> <span class="o">(</span><span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">-</span> <span class="mi">5</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="even-or-odd">
<span id="id9"></span><h3><span class="section-number">3.1.9. </span>Example<a class="headerlink" href="#even-or-odd" title="Permalink to this headline">&#61633;</a></h3>
<p>In fact every integer is either even or odd; we will discuss how to prove this later, in
<a class="reference internal" href="04_Proofs_with_Structure_II.html#even-or-odd-proof"><span class="std std-numref">Example 4.2.9</span></a>.</p>
<p>In Lean this fact can be invoked as the lemma <code class="docutils literal notranslate"><span class="pre">Int.even_or_odd</span></code>:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">lemma</span> <span class="n">Int.even_or_odd</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="n">Even</span> <span class="n">n</span> <span class="bp">&#8744;</span> <span class="n">Odd</span> <span class="n">n</span> <span class="o">:=</span>
</pre></div>
</div>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(n\)</span> be an integer. Prove that <span class="math notranslate nohighlight">\(n ^ 2 + n + 4\)</span> is even.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We consider two cases, depending on whether <span class="math notranslate nohighlight">\(n\)</span> is even or odd.</p>
<p>If <span class="math notranslate nohighlight">\(n\)</span> is even, then there exists an integer <span class="math notranslate nohighlight">\(x\)</span> such that <span class="math notranslate nohighlight">\(n=2x\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}n ^ 2 + n + 4 &amp;= (2 x) ^ 2 + 2  x + 4\\
&amp;= 2  (2 x ^ 2 + x + 2),\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(n ^ 2 + n + 4\)</span> is even.</p>
<p>If <span class="math notranslate nohighlight">\(n\)</span> is odd, then there exists an integer <span class="math notranslate nohighlight">\(x\)</span> such that <span class="math notranslate nohighlight">\(n=2x+1\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}n ^ 2 + n + 4 &amp;= (2  x + 1) ^ 2 + (2  x + 1) + 4 \\
&amp;= 2 (2  x ^ 2 + 3 x + 3),\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(n ^ 2 + n + 4\)</span> is again even.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="n">Even</span> <span class="o">(</span><span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">4</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">obtain</span> <span class="n">hn</span> <span class="bp">|</span> <span class="n">hn</span> <span class="o">:=</span> <span class="n">Int.even_or_odd</span> <span class="n">n</span>
  <span class="bp">&#183;</span> <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">x</span><span class="o">,</span> <span class="n">hx</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hn</span>
    <span class="n">use</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">2</span>
    <span class="k">calc</span>
      <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">4</span> <span class="bp">=</span> <span class="o">(</span><span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span><span class="o">)</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">4</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hx</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="o">(</span><span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">2</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
  <span class="bp">&#183;</span> <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">x</span><span class="o">,</span> <span class="n">hx</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hn</span>
    <span class="n">use</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">3</span>
    <span class="k">calc</span>
      <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">4</span> <span class="bp">=</span> <span class="o">(</span><span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="o">(</span><span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">4</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hx</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="o">(</span><span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">3</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
</pre></div>
</div>
</section>
<section id="exercises">
<h3><span class="section-number">3.1.10. </span>Exercises<a class="headerlink" href="#exercises" title="Permalink to this headline">&#61633;</a></h3>
<ol class="arabic">
<li><p>Prove that -9 is odd.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Odd</span> <span class="o">(</span><span class="bp">-</span><span class="mi">9</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove that 26 is even.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Even</span> <span class="o">(</span><span class="mi">26</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(m\)</span> be an odd integer and <span class="math notranslate nohighlight">\(n\)</span> be an even integer.
Prove that <span class="math notranslate nohighlight">\(n + m\)</span> is odd.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">m</span> <span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hm</span> <span class="o">:</span> <span class="n">Odd</span> <span class="n">m</span><span class="o">)</span> <span class="o">(</span><span class="n">hn</span> <span class="o">:</span> <span class="n">Even</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="n">Odd</span> <span class="o">(</span><span class="n">n</span> <span class="bp">+</span> <span class="n">m</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(p\)</span> be an odd integer and let <span class="math notranslate nohighlight">\(q\)</span> be an even integer.  Show that
<span class="math notranslate nohighlight">\(p - q - 4\)</span> is odd.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">p</span> <span class="n">q</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hp</span> <span class="o">:</span> <span class="n">Odd</span> <span class="n">p</span><span class="o">)</span> <span class="o">(</span><span class="n">hq</span> <span class="o">:</span> <span class="n">Even</span> <span class="n">q</span><span class="o">)</span> <span class="o">:</span> <span class="n">Odd</span> <span class="o">(</span><span class="n">p</span> <span class="bp">-</span> <span class="n">q</span> <span class="bp">-</span> <span class="mi">4</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(a\)</span> be an even integer and let <span class="math notranslate nohighlight">\(b\)</span> be an odd integer.  Show that
<span class="math notranslate nohighlight">\(3a + b - 3\)</span> is even.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">ha</span> <span class="o">:</span> <span class="n">Even</span> <span class="n">a</span><span class="o">)</span> <span class="o">(</span><span class="n">hb</span> <span class="o">:</span> <span class="n">Odd</span> <span class="n">b</span><span class="o">)</span> <span class="o">:</span> <span class="n">Even</span> <span class="o">(</span><span class="mi">3</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">-</span> <span class="mi">3</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove that if the integers <span class="math notranslate nohighlight">\(r\)</span> and <span class="math notranslate nohighlight">\(s\)</span> are odd, then <span class="math notranslate nohighlight">\(3r-5s\)</span> is even.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">r</span> <span class="n">s</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hr</span> <span class="o">:</span> <span class="n">Odd</span> <span class="n">r</span><span class="o">)</span> <span class="o">(</span><span class="n">hs</span> <span class="o">:</span> <span class="n">Odd</span> <span class="n">s</span><span class="o">)</span> <span class="o">:</span> <span class="n">Even</span> <span class="o">(</span><span class="mi">3</span> <span class="bp">*</span> <span class="n">r</span> <span class="bp">-</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">s</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(x\)</span> be an integer.  Show that if <span class="math notranslate nohighlight">\(x\)</span> is odd then so is <span class="math notranslate nohighlight">\(x^3\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hx</span> <span class="o">:</span> <span class="n">Odd</span> <span class="n">x</span><span class="o">)</span> <span class="o">:</span> <span class="n">Odd</span> <span class="o">(</span><span class="n">x</span> <span class="bp">^</span> <span class="mi">3</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(n\)</span> be an odd integer.  Show that <span class="math notranslate nohighlight">\(n^2-3n+2\)</span> is even.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hn</span> <span class="o">:</span> <span class="n">Odd</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="n">Even</span> <span class="o">(</span><span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">2</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(a\)</span> be an integer and suppose that <span class="math notranslate nohighlight">\(a\)</span> is odd.  Show that <span class="math notranslate nohighlight">\(a^2+2a-4\)</span> is
odd.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">ha</span> <span class="o">:</span> <span class="n">Odd</span> <span class="n">a</span><span class="o">)</span> <span class="o">:</span> <span class="n">Odd</span> <span class="o">(</span><span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">-</span> <span class="mi">4</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(p\)</span> be an odd integer.  Show that <span class="math notranslate nohighlight">\(p^2+3p-5\)</span> is odd.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">p</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hp</span> <span class="o">:</span> <span class="n">Odd</span> <span class="n">p</span><span class="o">)</span> <span class="o">:</span> <span class="n">Odd</span> <span class="o">(</span><span class="n">p</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">p</span> <span class="bp">-</span> <span class="mi">5</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> be odd integers.  Show that <span class="math notranslate nohighlight">\(xy\)</span> is odd.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">x</span> <span class="n">y</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hx</span> <span class="o">:</span> <span class="n">Odd</span> <span class="n">x</span><span class="o">)</span> <span class="o">(</span><span class="n">hy</span> <span class="o">:</span> <span class="n">Odd</span> <span class="n">y</span><span class="o">)</span> <span class="o">:</span> <span class="n">Odd</span> <span class="o">(</span><span class="n">x</span> <span class="bp">*</span> <span class="n">y</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(n\)</span> be an integer.  Show that <span class="math notranslate nohighlight">\(3n^2+3n- 1\)</span> is odd.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="n">Odd</span> <span class="o">(</span><span class="mi">3</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">-</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(n\)</span> be an integer.  Show that there exists an integer <span class="math notranslate nohighlight">\(m\geq n\)</span> which is odd.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">m</span> <span class="bp">&#8805;</span> <span class="n">n</span><span class="o">,</span> <span class="n">Odd</span> <span class="n">m</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(a\)</span>, <span class="math notranslate nohighlight">\(b\)</span> and <span class="math notranslate nohighlight">\(c\)</span> be integers.  Show that at least one of <span class="math notranslate nohighlight">\(a-b\)</span>,
<span class="math notranslate nohighlight">\(a+c\)</span> or <span class="math notranslate nohighlight">\(b-c\)</span> is even. <a class="footnote-reference brackets" href="#id11" id="id10">1</a></p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="n">Even</span> <span class="o">(</span><span class="n">a</span> <span class="bp">-</span> <span class="n">b</span><span class="o">)</span> <span class="bp">&#8744;</span> <span class="n">Even</span> <span class="o">(</span><span class="n">a</span> <span class="bp">+</span> <span class="n">c</span><span class="o">)</span> <span class="bp">&#8744;</span> <span class="n">Even</span> <span class="o">(</span><span class="n">b</span> <span class="bp">-</span> <span class="n">c</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
</ol>
<p class="rubric">Footnotes</p>
<dl class="footnote brackets">
<dt class="label" id="id11"><span class="brackets"><a class="fn-backref" href="#id10">1</a></span></dt>
<dd><p>Exercise taken from Hammack,
<a class="reference external" href="https://www.people.vcu.edu/~rhammack/BookOfProof/">Book of Proof</a>, Chapter 9.</p>
</dd>
</dl>
</section>
</section>
<section id="divisibility">
<span id="id12"></span><h2><span class="section-number">3.2. </span>Divisibility<a class="headerlink" href="#divisibility" title="Permalink to this headline">&#61633;</a></h2>
<section id="id13">
<h3><span class="section-number">3.2.1. </span>Example<a class="headerlink" href="#id13" title="Permalink to this headline">&#61633;</a></h3>
<p>Another mathematical definition you may have seen before is the definition of divisibility.</p>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>A natural number <span class="math notranslate nohighlight">\(b\)</span> <em>is divisible by</em> another natural number <span class="math notranslate nohighlight">\(a\)</span>, if there exists
a natural number <span class="math notranslate nohighlight">\(c\)</span>, such that <span class="math notranslate nohighlight">\(b=ac\)</span>.</p>
</div>
<p>For example,</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that the natural number 88 is divisible by 11.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p><span class="math notranslate nohighlight">\(88 = 11 \cdot 8\)</span>.</p>
</div>
<p>Divisibility is a very important concept, and there are several different names for it.  All the
following mean the same thing:</p>
<ul class="simple">
<li><p><span class="math notranslate nohighlight">\(b\)</span> <em>is divisible by</em> <span class="math notranslate nohighlight">\(a\)</span></p></li>
<li><p><span class="math notranslate nohighlight">\(b\)</span> <em>is a multiple of</em> <span class="math notranslate nohighlight">\(a\)</span></p></li>
<li><p><span class="math notranslate nohighlight">\(a\)</span> <em>is a divisor of</em> <span class="math notranslate nohighlight">\(b\)</span></p></li>
<li><p><span class="math notranslate nohighlight">\(a\)</span> <em>is a factor of</em> <span class="math notranslate nohighlight">\(b\)</span></p></li>
<li><p><span class="math notranslate nohighlight">\(a\)</span> <em>divides</em> <span class="math notranslate nohighlight">\(b\)</span></p></li>
</ul>
<p>We will most frequently use the last of these, &#8220;<span class="math notranslate nohighlight">\(a\)</span> <em>divides</em> <span class="math notranslate nohighlight">\(b\)</span>,&#8221; since it&#8217;s the most
compact.  There is also a standard notation, <span class="math notranslate nohighlight">\(a \mid b\)</span>, which we will also use frequently.</p>
<p>In Lean, the definition of divisibility is already in the library,
together with many theorems about it.  We will typically work with this definition in Lean using
the notation, <code class="docutils literal notranslate"><span class="pre">&#8739;</span></code>, which you can type in Lean as <code class="docutils literal notranslate"><span class="pre">\|</span></code> or <code class="docutils literal notranslate"><span class="pre">\mid</span></code>.  (In general, hover over a
symbol in VSCode with your mouse to find out how to type it.)  Warning: this is different from the
visually similar symbol <code class="docutils literal notranslate"><span class="pre">|</span></code> which appears on your keyboard and which we use in <code class="docutils literal notranslate"><span class="pre">obtain</span></code>
statements.</p>
<p>As in <a class="reference internal" href="#parity"><span class="std std-numref">Section 3.1</span></a> with <code class="docutils literal notranslate"><span class="pre">dsimp</span> <span class="pre">[Odd]</span></code>, it is possible to unfold the definition of
divisibility in the middle of a Lean proof to remind yourself of what it means in the current
context.  You can write either <code class="docutils literal notranslate"><span class="pre">dsimp</span> <span class="pre">[Dvd.dvd]</span></code> (this being the text name of the Lean notation
<span class="math notranslate nohighlight">\(\mid\)</span> for divisibility) or <code class="docutils literal notranslate"><span class="pre">dsimp</span> <span class="pre">[(&#183;</span> <span class="pre">&#8739;</span> <span class="pre">&#183;)]</span></code> &#8211; unfortunately <code class="docutils literal notranslate"><span class="pre">dsimp</span> <span class="pre">[&#8739;]</span></code> without the
dots and parentheses does not work. As in the <a class="reference internal" href="#parity"><span class="std std-numref">Section 3.1</span></a> examples, this unfolding
is optional &#8211; the proof still works without it.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">(</span><span class="mi">11</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="bp">&#8739;</span> <span class="mi">88</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[(</span><span class="bp">&#183;</span> <span class="bp">&#8739;</span> <span class="bp">&#183;</span><span class="o">)]</span>
  <span class="n">use</span> <span class="mi">8</span>
  <span class="n">numbers</span>
</pre></div>
</div>
</section>
<section id="id14">
<h3><span class="section-number">3.2.2. </span>Example<a class="headerlink" href="#id14" title="Permalink to this headline">&#61633;</a></h3>
<p>Another feature of this definition is that, although we stated it above for natural numbers, we
will also often want to consider divisibility of integers.  Here is the corresponding definition for
integers:</p>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>An integer <span class="math notranslate nohighlight">\(b\)</span> <em>is divisible by</em> another integer <span class="math notranslate nohighlight">\(a\)</span>, if there exists an integer
<span class="math notranslate nohighlight">\(c\)</span>, such that <span class="math notranslate nohighlight">\(b=ac\)</span>.</p>
</div>
<p>We also use all the same variant terminology and the same notation <span class="math notranslate nohighlight">\(a \mid b\)</span> for integer
divisibility.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that the integer 6 is divisible by -2.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p><span class="math notranslate nohighlight">\(6 = -2 \cdot -3\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="o">(</span><span class="bp">-</span><span class="mi">2</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8739;</span> <span class="mi">6</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="id15">
<h3><span class="section-number">3.2.3. </span>Example<a class="headerlink" href="#id15" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> be integers and suppose that <span class="math notranslate nohighlight">\(a \mid b\)</span>.  Show that
<span class="math notranslate nohighlight">\(a \mid b^2+2b\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Since <span class="math notranslate nohighlight">\(a \mid b\)</span>, there exists an integer <span class="math notranslate nohighlight">\(k\)</span> such that <span class="math notranslate nohighlight">\(b=ak\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}b ^ 2 + 2 b &amp;= (a k) ^ 2 + 2 (a k) \\
&amp; = a (k (a k + 2)).\end{split}\]</div>
<p>So <span class="math notranslate nohighlight">\(a \mid b^2+2b\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hab</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8739;</span> <span class="n">b</span><span class="o">)</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8739;</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">k</span><span class="o">,</span> <span class="n">hk</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hab</span>
  <span class="n">use</span> <span class="n">k</span> <span class="bp">*</span> <span class="o">(</span><span class="n">a</span> <span class="bp">*</span> <span class="n">k</span> <span class="bp">+</span> <span class="mi">2</span><span class="o">)</span>
  <span class="k">calc</span>
    <span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">=</span> <span class="o">(</span><span class="n">a</span> <span class="bp">*</span> <span class="n">k</span><span class="o">)</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="o">(</span><span class="n">a</span> <span class="bp">*</span> <span class="n">k</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hk</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="n">a</span> <span class="bp">*</span> <span class="o">(</span><span class="n">k</span> <span class="bp">*</span> <span class="o">(</span><span class="n">a</span> <span class="bp">*</span> <span class="n">k</span> <span class="bp">+</span> <span class="mi">2</span><span class="o">))</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
</pre></div>
</div>
</section>
<section id="id16">
<h3><span class="section-number">3.2.4. </span>Example<a class="headerlink" href="#id16" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(a\)</span>, <span class="math notranslate nohighlight">\(b\)</span> and <span class="math notranslate nohighlight">\(c\)</span> be natural numbers and suppose that <span class="math notranslate nohighlight">\(a \mid b\)</span> and
<span class="math notranslate nohighlight">\(b ^2\mid c\)</span>.  Show that <span class="math notranslate nohighlight">\(a^2 \mid c\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Since <span class="math notranslate nohighlight">\(a \mid b\)</span>, there exists a natural number <span class="math notranslate nohighlight">\(x\)</span> such that <span class="math notranslate nohighlight">\(b=ax\)</span>.
Since <span class="math notranslate nohighlight">\(b^2 \mid c\)</span>, there exists a natural number <span class="math notranslate nohighlight">\(y\)</span> such that <span class="math notranslate nohighlight">\(c=b^2y\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}c &amp;= b ^ 2 y \\
&amp; = (a x) ^ 2 y\\
&amp; = a ^ 2 (x ^ 2 y).\end{split}\]</div>
<p>So <span class="math notranslate nohighlight">\(a ^2 \mid c\)</span>.</p>
</div>
<p>Translate this solution into Lean.
As usual, if you wish, you can use the command <code class="docutils literal notranslate"><span class="pre">dsimp</span> <span class="pre">[(&#183;</span> <span class="pre">&#8739;</span> <span class="pre">&#183;)]</span> <span class="pre">at</span> <span class="pre">*</span></code> to unfold <span class="math notranslate nohighlight">\(\mid\)</span> to
its definition everywhere in the goal state, though this will have no effect on the correctness of
the proof.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">}</span> <span class="o">(</span><span class="n">hab</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8739;</span> <span class="n">b</span><span class="o">)</span> <span class="o">(</span><span class="n">hbc</span> <span class="o">:</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8739;</span> <span class="n">c</span><span class="o">)</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8739;</span> <span class="n">c</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="id17">
<h3><span class="section-number">3.2.5. </span>Example<a class="headerlink" href="#id17" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(x\)</span>, <span class="math notranslate nohighlight">\(y\)</span> and <span class="math notranslate nohighlight">\(z\)</span> be natural numbers and suppose that <span class="math notranslate nohighlight">\(xy \mid z\)</span>.
Show that <span class="math notranslate nohighlight">\(x \mid z\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Since <span class="math notranslate nohighlight">\(xy \mid z\)</span>, there exists a natural number <span class="math notranslate nohighlight">\(t\)</span> such that <span class="math notranslate nohighlight">\(z=(xy)t\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}z &amp;= (xy)t \\
&amp; = x(yt).\end{split}\]</div>
<p>So <span class="math notranslate nohighlight">\(x \mid z\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">x</span> <span class="n">y</span> <span class="n">z</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">}</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">x</span> <span class="bp">*</span> <span class="n">y</span> <span class="bp">&#8739;</span> <span class="n">z</span><span class="o">)</span> <span class="o">:</span> <span class="n">x</span> <span class="bp">&#8739;</span> <span class="n">z</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="not-divisible">
<span id="id18"></span><h3><span class="section-number">3.2.6. </span>Example<a class="headerlink" href="#not-divisible" title="Permalink to this headline">&#61633;</a></h3>
<p>You might wonder how to show that a number is <em>not</em> divisible by another number.  A convenient test
here is a theorem which we will prove later in the book, in
<a class="reference internal" href="04_Proofs_with_Structure_II.html#not-divisible-proof"><span class="std std-numref">Example 4.5.8</span></a>: if an integer <span class="math notranslate nohighlight">\(a\)</span> is strictly between two
consecutive multiples of an integer <span class="math notranslate nohighlight">\(b\)</span>, then it is not a multiple of
<span class="math notranslate nohighlight">\(b\)</span>.  More formally, if there exists an integer <span class="math notranslate nohighlight">\(q\)</span> such that
<span class="math notranslate nohighlight">\(bq&lt;a&lt;b(q + 1)\)</span>, then <span class="math notranslate nohighlight">\(a\)</span> is not a multiple of <span class="math notranslate nohighlight">\(b\)</span>.  Here is an
example applying this test:</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that 12 is not divisible by 5.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p><span class="math notranslate nohighlight">\(5 \cdot 2 &lt; 12 &lt; 5 \cdot (2 + 1)\)</span>.</p>
</div>
<p>In Lean, this test is available as the lemma <code class="docutils literal notranslate"><span class="pre">Int.not_dvd_of_exists_lt_and_lt</span></code>:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">lemma</span> <span class="n">Int.not_dvd_of_exists_lt_and_lt</span> <span class="o">(</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span>
  <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">q</span><span class="o">,</span> <span class="n">b</span> <span class="bp">*</span> <span class="n">q</span> <span class="bp">&lt;</span> <span class="n">a</span> <span class="bp">&#8743;</span> <span class="n">a</span> <span class="bp">&lt;</span> <span class="n">b</span> <span class="bp">*</span> <span class="o">(</span><span class="n">q</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">))</span> <span class="o">:</span>
  <span class="bp">&#172;</span><span class="n">b</span> <span class="bp">&#8739;</span> <span class="n">a</span> <span class="o">:=</span>
</pre></div>
</div>
<p>And here is the same solution written up in Lean.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span><span class="o">(</span><span class="mi">5</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8739;</span> <span class="mi">12</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">apply</span> <span class="n">Int.not_dvd_of_exists_lt_and_lt</span>
  <span class="n">use</span> <span class="mi">2</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span> <span class="c1">-- show `5 * 2 &lt; 12`</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span> <span class="c1">-- show `12 &lt; 5 * (2 + 1)`</span>
</pre></div>
</div>
</section>
<section id="dvd-bd-1">
<span id="id19"></span><h3><span class="section-number">3.2.7. </span>Example<a class="headerlink" href="#dvd-bd-1" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> be natural numbers, with <span class="math notranslate nohighlight">\(b\)</span> positive, and suppose that
<span class="math notranslate nohighlight">\(a\)</span> divides <span class="math notranslate nohighlight">\(b\)</span>.  Show that <span class="math notranslate nohighlight">\(a \le b\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Since <span class="math notranslate nohighlight">\(a \mid b\)</span>, there exists a natural number <span class="math notranslate nohighlight">\(k\)</span> such that <span class="math notranslate nohighlight">\(b=ak\)</span>.</p>
<p>We first note that</p>
<div class="math notranslate nohighlight">
\[0 &lt; b =ak\]</div>
<p>so <span class="math notranslate nohighlight">\(0&lt;k\)</span>. Thus in fact <span class="math notranslate nohighlight">\(1 \le k\)</span>.</p>
<p>Now, we have</p>
<div class="math notranslate nohighlight">
\[\begin{split}a &amp;= a \cdot 1 \\
&amp;&#8804; a k \\
&amp;= b.\end{split}\]</div>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">}</span> <span class="o">(</span><span class="n">hb</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">b</span><span class="o">)</span> <span class="o">(</span><span class="n">hab</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8739;</span> <span class="n">b</span><span class="o">)</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8804;</span> <span class="n">b</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">k</span><span class="o">,</span> <span class="n">hk</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hab</span>
  <span class="k">have</span> <span class="n">H1</span> <span class="o">:=</span>
    <span class="k">calc</span>
      <span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">b</span> <span class="o">:=</span> <span class="n">hb</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">k</span> <span class="o">:=</span> <span class="n">hk</span>
  <span class="n">cancel</span> <span class="n">a</span> <span class="n">at</span> <span class="n">H1</span>
  <span class="k">have</span> <span class="n">H</span> <span class="o">:</span> <span class="mi">1</span> <span class="bp">&#8804;</span> <span class="n">k</span> <span class="o">:=</span> <span class="n">H1</span>
  <span class="k">calc</span>
    <span class="n">a</span> <span class="bp">=</span> <span class="n">a</span> <span class="bp">*</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">_</span> <span class="bp">&#8804;</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">k</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">H</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="n">b</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hk</span><span class="o">]</span>
</pre></div>
</div>
<p>This lemma is available in the main Lean library under the name <code class="docutils literal notranslate"><span class="pre">Nat.le_of_dvd</span></code>.</p>
</section>
<section id="dvd-bd-2">
<span id="id20"></span><h3><span class="section-number">3.2.8. </span>Example<a class="headerlink" href="#dvd-bd-2" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> be natural numbers, with <span class="math notranslate nohighlight">\(b\)</span> positive, and suppose that
<span class="math notranslate nohighlight">\(a\)</span> divides <span class="math notranslate nohighlight">\(b\)</span>.  Show that <span class="math notranslate nohighlight">\(a\)</span> is positive.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Since <span class="math notranslate nohighlight">\(a \mid b\)</span>, there exists a natural number <span class="math notranslate nohighlight">\(k\)</span> such that <span class="math notranslate nohighlight">\(b=ak\)</span>.</p>
<p>We have</p>
<div class="math notranslate nohighlight">
\[0 &lt; b = a k,\]</div>
<p>so <span class="math notranslate nohighlight">\(0&lt;a\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">}</span> <span class="o">(</span><span class="n">hab</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8739;</span> <span class="n">b</span><span class="o">)</span> <span class="o">(</span><span class="n">hb</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">b</span><span class="o">)</span> <span class="o">:</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">a</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
<p>This lemma is also available in the main Lean library, under the name <code class="docutils literal notranslate"><span class="pre">Nat.pos_of_dvd_of_pos</span></code>.</p>
</section>
<section id="id21">
<h3><span class="section-number">3.2.9. </span>Exercises<a class="headerlink" href="#id21" title="Permalink to this headline">&#61633;</a></h3>
<ol class="arabic">
<li><p>Show that 0 is divisible by every integer <span class="math notranslate nohighlight">\(t\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">t</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="n">t</span> <span class="bp">&#8739;</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Show that -10 is not divisible by 3.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span><span class="o">(</span><span class="mi">3</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8739;</span> <span class="bp">-</span><span class="mi">10</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> be integers and suppose that <span class="math notranslate nohighlight">\(x \mid y\)</span>.  Show that
<span class="math notranslate nohighlight">\(x \mid 3y-4y^2\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">x</span> <span class="n">y</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">x</span> <span class="bp">&#8739;</span> <span class="n">y</span><span class="o">)</span> <span class="o">:</span> <span class="n">x</span> <span class="bp">&#8739;</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">y</span> <span class="bp">-</span> <span class="mi">4</span> <span class="bp">*</span> <span class="n">y</span> <span class="bp">^</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(m\)</span> and <span class="math notranslate nohighlight">\(n\)</span> be integers and suppose that <span class="math notranslate nohighlight">\(m \mid n\)</span>.  Show that
<span class="math notranslate nohighlight">\(m \mid 2n^3+n\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">m</span> <span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">m</span> <span class="bp">&#8739;</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="n">m</span> <span class="bp">&#8739;</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">+</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> be integers and suppose that <span class="math notranslate nohighlight">\(a \mid b\)</span>.  Show that
<span class="math notranslate nohighlight">\(a \mid 2b^3-b^2+3b\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hab</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8739;</span> <span class="n">b</span><span class="o">)</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8739;</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">-</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">b</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(k\)</span>, <span class="math notranslate nohighlight">\(l\)</span> and <span class="math notranslate nohighlight">\(m\)</span> be integers and suppose that <span class="math notranslate nohighlight">\(k\)</span> divides <span class="math notranslate nohighlight">\(l\)</span>
and <span class="math notranslate nohighlight">\(l^3\)</span> divides <span class="math notranslate nohighlight">\(m\)</span>.  Show that <span class="math notranslate nohighlight">\(k^3\)</span> divides <span class="math notranslate nohighlight">\(m\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">k</span> <span class="n">l</span> <span class="n">m</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">h1</span> <span class="o">:</span> <span class="n">k</span> <span class="bp">&#8739;</span> <span class="n">l</span><span class="o">)</span> <span class="o">(</span><span class="n">h2</span> <span class="o">:</span> <span class="n">l</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">&#8739;</span> <span class="n">m</span><span class="o">)</span> <span class="o">:</span> <span class="n">k</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">&#8739;</span> <span class="n">m</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(p\)</span>, <span class="math notranslate nohighlight">\(q\)</span> and <span class="math notranslate nohighlight">\(r\)</span> be integers and suppose that <span class="math notranslate nohighlight">\(p^3\)</span> divides <span class="math notranslate nohighlight">\(q\)</span>
and <span class="math notranslate nohighlight">\(q^2\)</span> divides <span class="math notranslate nohighlight">\(r\)</span>.  Show that <span class="math notranslate nohighlight">\(p^6\)</span> divides <span class="math notranslate nohighlight">\(r\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">p</span> <span class="n">q</span> <span class="n">r</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hpq</span> <span class="o">:</span> <span class="n">p</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">&#8739;</span> <span class="n">q</span><span class="o">)</span> <span class="o">(</span><span class="n">hqr</span> <span class="o">:</span> <span class="n">q</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8739;</span> <span class="n">r</span><span class="o">)</span> <span class="o">:</span> <span class="n">p</span> <span class="bp">^</span> <span class="mi">6</span> <span class="bp">&#8739;</span> <span class="n">r</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Show that there exists a natural number <span class="math notranslate nohighlight">\(n&gt;0\)</span>, such that <span class="math notranslate nohighlight">\(9\)</span> is a factor of
<span class="math notranslate nohighlight">\(2^n-1\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">,</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">n</span> <span class="bp">&#8743;</span> <span class="mi">9</span> <span class="bp">&#8739;</span> <span class="mi">2</span> <span class="bp">^</span> <span class="n">n</span> <span class="bp">-</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Show that there exists integers <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span>, with <span class="math notranslate nohighlight">\(0&lt;b&lt;a\)</span>, such that
<span class="math notranslate nohighlight">\(a-b \mid a+b\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">,</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">b</span> <span class="bp">&#8743;</span> <span class="n">b</span> <span class="bp">&lt;</span> <span class="n">a</span> <span class="bp">&#8743;</span> <span class="n">a</span> <span class="bp">-</span> <span class="n">b</span> <span class="bp">&#8739;</span> <span class="n">a</span> <span class="bp">+</span> <span class="n">b</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
</ol>
</section>
</section>
<section id="modular-arithmetic-theory">
<span id="theory-modular"></span><h2><span class="section-number">3.3. </span>Modular arithmetic: theory<a class="headerlink" href="#modular-arithmetic-theory" title="Permalink to this headline">&#61633;</a></h2>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>The integers <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> are <em>congruent modulo</em> <span class="math notranslate nohighlight">\(n\)</span>, if <span class="math notranslate nohighlight">\(n\mid (a - b)\)</span>.</p>
</div>
<p>We use the notation <span class="math notranslate nohighlight">\(a\equiv b \mod n\)</span> to denote that <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> are congruent
modulo <span class="math notranslate nohighlight">\(n\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">Int.ModEq</span> <span class="o">(</span><span class="n">n</span> <span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="kt">Prop</span> <span class="o">:=</span> <span class="n">n</span> <span class="bp">&#8739;</span> <span class="n">a</span> <span class="bp">-</span> <span class="n">b</span>

<span class="kd">notation</span><span class="o">:</span><span class="mi">50</span> <span class="n">a</span> <span class="s2">&quot; &#8801; &quot;</span> <span class="n">b</span> <span class="s2">&quot; [ZMOD &quot;</span> <span class="n">n</span> <span class="s2">&quot;]&quot;</span> <span class="bp">=&gt;</span> <span class="n">Int.ModEq</span> <span class="n">n</span> <span class="n">a</span> <span class="n">b</span>
</pre></div>
</div>
<section id="id22">
<h3><span class="section-number">3.3.1. </span>Example<a class="headerlink" href="#id22" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that <span class="math notranslate nohighlight">\(11\equiv 3 \mod 4\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p><span class="math notranslate nohighlight">\(11-3=4\cdot 2\)</span>, so <span class="math notranslate nohighlight">\(4\mid(11-3)\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="mi">11</span> <span class="bp">&#8801;</span> <span class="mi">3</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">4</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">use</span> <span class="mi">2</span>
  <span class="n">numbers</span>
</pre></div>
</div>
</section>
<section id="id23">
<h3><span class="section-number">3.3.2. </span>Example<a class="headerlink" href="#id23" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that <span class="math notranslate nohighlight">\(-5\equiv 1 \mod 3\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p><span class="math notranslate nohighlight">\(-5-1=3\cdot -2\)</span>, so <span class="math notranslate nohighlight">\(3\mid(-5-1)\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">-</span><span class="mi">5</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="modeq-add">
<span id="id24"></span><h3><span class="section-number">3.3.3. </span>Example<a class="headerlink" href="#modeq-add" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-lemma-addition-rule-for-modular-arithmetic admonition">
<p class="admonition-title">Lemma (addition rule for modular arithmetic)</p>
<p>Let <span class="math notranslate nohighlight">\(a\)</span>, <span class="math notranslate nohighlight">\(b\)</span>, <span class="math notranslate nohighlight">\(c\)</span>, <span class="math notranslate nohighlight">\(d\)</span> and <span class="math notranslate nohighlight">\(n\)</span> be integers, and suppose that
<span class="math notranslate nohighlight">\(a\equiv b \mod n\)</span> and <span class="math notranslate nohighlight">\(c\equiv d \mod n\)</span>.  Then <span class="math notranslate nohighlight">\(a+c\equiv b+d \mod n\)</span>.</p>
</div>
<div class="admonition-proof admonition">
<p class="admonition-title">Proof</p>
<p>Since <span class="math notranslate nohighlight">\(a\equiv b \mod n\)</span>, there exists an integer <span class="math notranslate nohighlight">\(x\)</span> such that <span class="math notranslate nohighlight">\(a-b=nx\)</span>.
Since <span class="math notranslate nohighlight">\(c\equiv d \mod n\)</span>, there exists an integer <span class="math notranslate nohighlight">\(y\)</span> such that <span class="math notranslate nohighlight">\(c-d=ny\)</span>.
Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}a + c - (b + d) &amp;= (a - b) + (c - d) \\
&amp;= n x + n y \\
&amp;= n (x + y),\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(a+c\equiv b+d \mod n\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">Int.ModEq.add</span> <span class="o">{</span><span class="n">n</span> <span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="n">d</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">h1</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="n">b</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">])</span> <span class="o">(</span><span class="n">h2</span> <span class="o">:</span> <span class="n">c</span> <span class="bp">&#8801;</span> <span class="n">d</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">])</span> <span class="o">:</span>
    <span class="n">a</span> <span class="bp">+</span> <span class="n">c</span> <span class="bp">&#8801;</span> <span class="n">b</span> <span class="bp">+</span> <span class="n">d</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Int.ModEq</span><span class="o">]</span> <span class="n">at</span> <span class="bp">*</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">x</span><span class="o">,</span> <span class="n">hx</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h1</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">y</span><span class="o">,</span> <span class="n">hy</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h2</span>
  <span class="n">use</span> <span class="n">x</span> <span class="bp">+</span> <span class="n">y</span>
  <span class="k">calc</span>
    <span class="n">a</span> <span class="bp">+</span> <span class="n">c</span> <span class="bp">-</span> <span class="o">(</span><span class="n">b</span> <span class="bp">+</span> <span class="n">d</span><span class="o">)</span> <span class="bp">=</span> <span class="n">a</span> <span class="bp">-</span> <span class="n">b</span> <span class="bp">+</span> <span class="o">(</span><span class="n">c</span> <span class="bp">-</span> <span class="n">d</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="n">n</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">+</span> <span class="n">n</span> <span class="bp">*</span> <span class="n">y</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hx</span><span class="o">,</span> <span class="n">hy</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="n">n</span> <span class="bp">*</span> <span class="o">(</span><span class="n">x</span> <span class="bp">+</span> <span class="n">y</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
</pre></div>
</div>
</section>
<section id="exercise">
<h3><span class="section-number">3.3.4. </span>Exercise<a class="headerlink" href="#exercise" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-lemma-subtraction-rule-for-modular-arithmetic admonition">
<p class="admonition-title">Lemma (subtraction rule for modular arithmetic)</p>
<p>Let <span class="math notranslate nohighlight">\(a\)</span>, <span class="math notranslate nohighlight">\(b\)</span>, <span class="math notranslate nohighlight">\(c\)</span>, <span class="math notranslate nohighlight">\(d\)</span> and <span class="math notranslate nohighlight">\(n\)</span> be integers, and suppose that
<span class="math notranslate nohighlight">\(a\equiv b \mod n\)</span> and <span class="math notranslate nohighlight">\(c\equiv d \mod n\)</span>.  Then <span class="math notranslate nohighlight">\(a-c\equiv b-d \mod n\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">Int.ModEq.sub</span> <span class="o">{</span><span class="n">n</span> <span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="n">d</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">h1</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="n">b</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">])</span> <span class="o">(</span><span class="n">h2</span> <span class="o">:</span> <span class="n">c</span> <span class="bp">&#8801;</span> <span class="n">d</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">])</span> <span class="o">:</span>
    <span class="n">a</span> <span class="bp">-</span> <span class="n">c</span> <span class="bp">&#8801;</span> <span class="n">b</span> <span class="bp">-</span> <span class="n">d</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="id25">
<h3><span class="section-number">3.3.5. </span>Exercise<a class="headerlink" href="#id25" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-lemma-negation-rule-for-modular-arithmetic admonition">
<p class="admonition-title">Lemma (negation rule for modular arithmetic)</p>
<p>Let <span class="math notranslate nohighlight">\(a\)</span>, <span class="math notranslate nohighlight">\(b\)</span> and <span class="math notranslate nohighlight">\(n\)</span> be integers, and suppose that
<span class="math notranslate nohighlight">\(a\equiv b \mod n\)</span>.  Then <span class="math notranslate nohighlight">\(-a\equiv -b \mod n\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">Int.ModEq.neg</span> <span class="o">{</span><span class="n">n</span> <span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">h1</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="n">b</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">])</span> <span class="o">:</span> <span class="bp">-</span><span class="n">a</span> <span class="bp">&#8801;</span> <span class="bp">-</span><span class="n">b</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="modeq-mul">
<span id="id26"></span><h3><span class="section-number">3.3.6. </span>Example<a class="headerlink" href="#modeq-mul" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-lemma-multiplication-rule-for-modular-arithmetic admonition">
<p class="admonition-title">Lemma (multiplication rule for modular arithmetic)</p>
<p>Let <span class="math notranslate nohighlight">\(a\)</span>, <span class="math notranslate nohighlight">\(b\)</span>, <span class="math notranslate nohighlight">\(c\)</span>, <span class="math notranslate nohighlight">\(d\)</span> and <span class="math notranslate nohighlight">\(n\)</span> be integers, and suppose that
<span class="math notranslate nohighlight">\(a\equiv b \mod n\)</span> and <span class="math notranslate nohighlight">\(c\equiv d \mod n\)</span>.  Then <span class="math notranslate nohighlight">\(ac\equiv bd \mod n\)</span>.</p>
</div>
<div class="admonition-proof admonition">
<p class="admonition-title">Proof</p>
<p>Since <span class="math notranslate nohighlight">\(a\equiv b \mod n\)</span>, there exists an integer <span class="math notranslate nohighlight">\(x\)</span> such that <span class="math notranslate nohighlight">\(a-b=nx\)</span>.
Since <span class="math notranslate nohighlight">\(c\equiv d \mod n\)</span>, there exists an integer <span class="math notranslate nohighlight">\(y\)</span> such that <span class="math notranslate nohighlight">\(c-d=ny\)</span>.
Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}a c - b d &amp;= (a - b) c + b (c - d) \\
&amp;= (n x)  c + b  (n y) \\
&amp; = n (x c + b y),\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(ac\equiv bd \mod n\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">Int.ModEq.mul</span> <span class="o">{</span><span class="n">n</span> <span class="n">a</span> <span class="n">b</span> <span class="n">c</span> <span class="n">d</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">h1</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="n">b</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">])</span> <span class="o">(</span><span class="n">h2</span> <span class="o">:</span> <span class="n">c</span> <span class="bp">&#8801;</span> <span class="n">d</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">])</span> <span class="o">:</span>
    <span class="n">a</span> <span class="bp">*</span> <span class="n">c</span> <span class="bp">&#8801;</span> <span class="n">b</span> <span class="bp">*</span> <span class="n">d</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">x</span><span class="o">,</span> <span class="n">hx</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h1</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">y</span><span class="o">,</span> <span class="n">hy</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h2</span>
  <span class="n">use</span> <span class="n">x</span> <span class="bp">*</span> <span class="n">c</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">*</span> <span class="n">y</span>
  <span class="k">calc</span>
    <span class="n">a</span> <span class="bp">*</span> <span class="n">c</span> <span class="bp">-</span> <span class="n">b</span> <span class="bp">*</span> <span class="n">d</span> <span class="bp">=</span> <span class="o">(</span><span class="n">a</span> <span class="bp">-</span> <span class="n">b</span><span class="o">)</span> <span class="bp">*</span> <span class="n">c</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">*</span> <span class="o">(</span><span class="n">c</span> <span class="bp">-</span> <span class="n">d</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="n">n</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">*</span> <span class="n">c</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">*</span> <span class="o">(</span><span class="n">n</span> <span class="bp">*</span> <span class="n">y</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hx</span><span class="o">,</span> <span class="n">hy</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="n">n</span> <span class="bp">*</span> <span class="o">(</span><span class="n">x</span> <span class="bp">*</span> <span class="n">c</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">*</span> <span class="n">y</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
</pre></div>
</div>
</section>
<section id="no-mod-division">
<span id="id27"></span><h3><span class="section-number">3.3.7. </span>Example<a class="headerlink" href="#no-mod-division" title="Permalink to this headline">&#61633;</a></h3>
<p>Warning:  There is no &#8220;division rule&#8221; for modular arithmetic!</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>It is possible to have integers <span class="math notranslate nohighlight">\(a\)</span>, <span class="math notranslate nohighlight">\(b\)</span>, <span class="math notranslate nohighlight">\(c\)</span>, <span class="math notranslate nohighlight">\(d\)</span> and <span class="math notranslate nohighlight">\(n\)</span> with
<span class="math notranslate nohighlight">\(a\equiv b \mod n\)</span> and <span class="math notranslate nohighlight">\(c\equiv d \mod n\)</span>, but <span class="math notranslate nohighlight">\(\frac{a}{c}\not\equiv \frac{b}{d} \mod n\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We can take <span class="math notranslate nohighlight">\(a=10\)</span>, <span class="math notranslate nohighlight">\(b=18\)</span>, <span class="math notranslate nohighlight">\(c=2\)</span>, <span class="math notranslate nohighlight">\(d=6\)</span>.  Indeed,</p>
<ul class="simple">
<li><p><span class="math notranslate nohighlight">\(10-18=4\cdot -2\)</span>, so <span class="math notranslate nohighlight">\(10\equiv 18 \mod 4\)</span>;</p></li>
<li><p><span class="math notranslate nohighlight">\(2-6=4\cdot -1\)</span>, so <span class="math notranslate nohighlight">\(2\equiv 6 \mod 4\)</span>;</p></li>
<li><p><span class="math notranslate nohighlight">\(\frac{10}{2}-\frac{18}{6}=2\)</span> lies between the consecutive multiples <span class="math notranslate nohighlight">\(4 \cdot 0\)</span> and
<span class="math notranslate nohighlight">\(4 \cdot (0 + 1)\)</span> of 4, so <span class="math notranslate nohighlight">\(\frac{10}{2}\not\equiv \frac{18}{6} \mod 4\)</span>.</p></li>
</ul>
</div>
<p>Notice that here we&#8217;re using the test for non-divisibility from
<a class="reference internal" href="#not-divisible"><span class="std std-numref">Example 3.2.6</span></a>.</p>
</section>
<section id="id28">
<h3><span class="section-number">3.3.8. </span>Example<a class="headerlink" href="#id28" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-lemma-squaring-rule-for-modular-arithmetic admonition">
<p class="admonition-title">Lemma (squaring rule for modular arithmetic)</p>
<p>Let <span class="math notranslate nohighlight">\(a\)</span>, <span class="math notranslate nohighlight">\(b\)</span> and <span class="math notranslate nohighlight">\(n\)</span> be integers, and suppose that
<span class="math notranslate nohighlight">\(a\equiv b \mod n\)</span>.  Then <span class="math notranslate nohighlight">\(a^2\equiv b^2 \mod n\)</span>.</p>
</div>
<div class="admonition-proof admonition">
<p class="admonition-title">Proof</p>
<p>Since <span class="math notranslate nohighlight">\(a\equiv b \mod n\)</span>, there exists an integer <span class="math notranslate nohighlight">\(x\)</span> such that <span class="math notranslate nohighlight">\(a-b=nx\)</span>.
Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}a ^ 2 - b ^ 2 &amp;= (a - b)  (a + b) \\
&amp;= (n x) (a + b) \\
&amp;= n  (x  (a + b)).\end{split}\]</div>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">Int.ModEq.pow_two</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="n">b</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">])</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8801;</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">x</span><span class="o">,</span> <span class="n">hx</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h</span>
  <span class="n">use</span> <span class="n">x</span> <span class="bp">*</span> <span class="o">(</span><span class="n">a</span> <span class="bp">+</span> <span class="n">b</span><span class="o">)</span>
  <span class="k">calc</span>
    <span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">=</span> <span class="o">(</span><span class="n">a</span> <span class="bp">-</span> <span class="n">b</span><span class="o">)</span> <span class="bp">*</span> <span class="o">(</span><span class="n">a</span> <span class="bp">+</span> <span class="n">b</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="n">n</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">*</span> <span class="o">(</span><span class="n">a</span> <span class="bp">+</span> <span class="n">b</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hx</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="n">n</span> <span class="bp">*</span> <span class="o">(</span><span class="n">x</span> <span class="bp">*</span> <span class="o">(</span><span class="n">a</span> <span class="bp">+</span> <span class="n">b</span><span class="o">))</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
</pre></div>
</div>
</section>
<section id="modeq-pow">
<span id="id29"></span><h3><span class="section-number">3.3.9. </span>Exercise<a class="headerlink" href="#modeq-pow" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-lemma-cubing-rule-for-modular-arithmetic admonition">
<p class="admonition-title">Lemma (cubing rule for modular arithmetic)</p>
<p>Let <span class="math notranslate nohighlight">\(a\)</span>, <span class="math notranslate nohighlight">\(b\)</span> and <span class="math notranslate nohighlight">\(n\)</span> be integers, and suppose that
<span class="math notranslate nohighlight">\(a\equiv b \mod n\)</span>.  Then <span class="math notranslate nohighlight">\(a^3\equiv b^3 \mod n\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">Int.ModEq.pow_three</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="n">b</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">])</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">&#8801;</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">3</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
<p>In fact the same is true for any power, although we don&#8217;t yet have the tools to prove it.  We&#8217;ll
come back to this later in the book, in <a class="reference internal" href="06_Induction.html#modeq-pow-proof"><span class="std std-numref">Example 6.1.3</span></a>.</p>
<div class="admonition-lemma-power-rule-for-modular-arithmetic admonition">
<p class="admonition-title">Lemma (power rule for modular arithmetic)</p>
<p>Let <span class="math notranslate nohighlight">\(k\)</span> be a natural number and let <span class="math notranslate nohighlight">\(a\)</span>, <span class="math notranslate nohighlight">\(b\)</span> and <span class="math notranslate nohighlight">\(n\)</span> be integers, and
suppose that <span class="math notranslate nohighlight">\(a\equiv b \mod n\)</span>.  Then <span class="math notranslate nohighlight">\(a^k\equiv b^k \mod n\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">Int.ModEq.pow</span> <span class="o">(</span><span class="n">k</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="n">b</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">])</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">^</span> <span class="n">k</span> <span class="bp">&#8801;</span> <span class="n">b</span> <span class="bp">^</span> <span class="n">k</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">]</span> <span class="o">:=</span>
  <span class="gr">sorry</span> <span class="c1">-- we&#39;ll prove this later in the book</span>
</pre></div>
</div>
</section>
<section id="modeq-refl">
<span id="id30"></span><h3><span class="section-number">3.3.10. </span>Example<a class="headerlink" href="#modeq-refl" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-lemma-reflexivity-rule-for-modular-arithmetic admonition">
<p class="admonition-title">Lemma (reflexivity rule for modular arithmetic)</p>
<p>Let <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(n\)</span> be integers. Then <span class="math notranslate nohighlight">\(a\equiv a \mod n\)</span>.</p>
</div>
<div class="admonition-proof admonition">
<p class="admonition-title">Proof</p>
<p><span class="math notranslate nohighlight">\(a-a=n\cdot 0\)</span>, so <span class="math notranslate nohighlight">\(n\mid a - a\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">Int.ModEq.refl</span> <span class="o">(</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="n">a</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">use</span> <span class="mi">0</span>
  <span class="n">ring</span>
</pre></div>
</div>
</section>
<section id="apply-mod-lemmas-example">
<span id="id31"></span><h3><span class="section-number">3.3.11. </span>Example<a class="headerlink" href="#apply-mod-lemmas-example" title="Permalink to this headline">&#61633;</a></h3>
<p>Whew! That was a lot of lemmas.  But they pay off, as you will now see.  Suppose we now encounter
some very specific modular arithmetic problem of the same general type as we&#8217;ve seen before: the
congruence modulo <span class="math notranslate nohighlight">\(n\)</span> of two expressions which differ in a kind of spot-the-difference way,
like a &#8220;rewriting&#8221; by one congruence.  For example,</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> be integers, and suppose that <span class="math notranslate nohighlight">\(a\equiv 2 \mod 4\)</span>.
Show that <span class="math notranslate nohighlight">\(a b ^ 2 + a ^ 2 b + 3 a \equiv 2 b ^ 2 + 2 ^ 2 \cdot b + 3 \cdot 2 \mod 4\)</span>.</p>
</div>
<p>We could solve this by working directly from the definition, which is rather painful:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">ha</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">4</span><span class="o">])</span> <span class="o">:</span>
    <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">*</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">4</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">x</span><span class="o">,</span> <span class="n">hx</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">ha</span>
  <span class="n">use</span> <span class="n">x</span> <span class="bp">*</span> <span class="o">(</span><span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">3</span><span class="o">)</span>
  <span class="k">calc</span>
    <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">-</span> <span class="o">(</span><span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">*</span> <span class="mi">2</span><span class="o">)</span> <span class="bp">=</span>
        <span class="o">(</span><span class="n">a</span> <span class="bp">-</span> <span class="mi">2</span><span class="o">)</span> <span class="bp">*</span> <span class="o">(</span><span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">3</span><span class="o">)</span> <span class="o">:=</span>
      <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">4</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">*</span> <span class="o">(</span><span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">3</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hx</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">4</span> <span class="bp">*</span> <span class="o">(</span><span class="n">x</span> <span class="bp">*</span> <span class="o">(</span><span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">3</span><span class="o">))</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
</pre></div>
</div>
<p>Or, better, we can solve this by applying the right combination of the lemmas we already proved,
in the right order.  This requires much less thinking:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">ha</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">4</span><span class="o">])</span> <span class="o">:</span>
    <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">*</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">4</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">apply</span> <span class="n">Int.ModEq.add</span>
  <span class="n">apply</span> <span class="n">Int.ModEq.add</span>
  <span class="n">apply</span> <span class="n">Int.ModEq.mul</span>
  <span class="n">apply</span> <span class="n">ha</span>
  <span class="n">apply</span> <span class="n">Int.ModEq.refl</span>
  <span class="n">apply</span> <span class="n">Int.ModEq.mul</span>
  <span class="n">apply</span> <span class="n">Int.ModEq.pow</span>
  <span class="n">apply</span> <span class="n">ha</span>
  <span class="n">apply</span> <span class="n">Int.ModEq.refl</span>
  <span class="n">apply</span> <span class="n">Int.ModEq.mul</span>
  <span class="n">apply</span> <span class="n">Int.ModEq.refl</span>
  <span class="n">apply</span> <span class="n">ha</span>
</pre></div>
</div>
</section>
<section id="id32">
<h3><span class="section-number">3.3.12. </span>Exercises<a class="headerlink" href="#id32" title="Permalink to this headline">&#61633;</a></h3>
<ol class="arabic">
<li><p>Show that <span class="math notranslate nohighlight">\(34\equiv 104 \mod 5\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="mi">34</span> <span class="bp">&#8801;</span> <span class="mi">104</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>(symmetry rule for modular arithmetic) Let <span class="math notranslate nohighlight">\(a\)</span>, <span class="math notranslate nohighlight">\(b\)</span> and <span class="math notranslate nohighlight">\(n\)</span> be integers, and
suppose that <span class="math notranslate nohighlight">\(a\equiv b \mod n\)</span>.  Show that <span class="math notranslate nohighlight">\(b\equiv a \mod n\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">Int.ModEq.symm</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="n">b</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">])</span> <span class="o">:</span> <span class="n">b</span> <span class="bp">&#8801;</span> <span class="n">a</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>(transitivity rule for modular arithmetic) Let <span class="math notranslate nohighlight">\(a\)</span>, <span class="math notranslate nohighlight">\(b\)</span>, <span class="math notranslate nohighlight">\(c\)</span> and <span class="math notranslate nohighlight">\(n\)</span> be
integers, and suppose that <span class="math notranslate nohighlight">\(a\equiv b \mod n\)</span> and <span class="math notranslate nohighlight">\(b\equiv c \mod n\)</span>.  Show that
<span class="math notranslate nohighlight">\(a\equiv c \mod n\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">Int.ModEq.trans</span> <span class="o">(</span><span class="n">h1</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="n">b</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">])</span> <span class="o">(</span><span class="n">h2</span> <span class="o">:</span> <span class="n">b</span> <span class="bp">&#8801;</span> <span class="n">c</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">])</span> <span class="o">:</span>
    <span class="n">a</span> <span class="bp">&#8801;</span> <span class="n">c</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(a\)</span>, <span class="math notranslate nohighlight">\(c\)</span> and <span class="math notranslate nohighlight">\(n\)</span> be integers.  Show that <span class="math notranslate nohighlight">\(a+nc\equiv a \mod n\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">+</span> <span class="n">n</span> <span class="bp">*</span> <span class="n">c</span> <span class="bp">&#8801;</span> <span class="n">a</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="n">n</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Give an alternative solution (i.e., with different numbers) to
<a class="reference internal" href="#no-mod-division"><span class="std std-numref">Example 3.3.7</span></a>.</p></li>
<li><p>Let <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> be integers, and suppose that <span class="math notranslate nohighlight">\(a \equiv b \mod 5\)</span>.  Show that
<span class="math notranslate nohighlight">\(2a+3 \equiv 2b+3 \mod 5\)</span>.</p>
<p>Give two solutions, following the style of the two solutions in
<a class="reference internal" href="#apply-mod-lemmas-example"><span class="std std-numref">Example 3.3.11</span></a>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="n">b</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">])</span> <span class="o">:</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">3</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(m\)</span> and <span class="math notranslate nohighlight">\(n\)</span> be integers, and suppose that <span class="math notranslate nohighlight">\(m \equiv n \mod 4\)</span>.  Show that
<span class="math notranslate nohighlight">\(3m-1 \equiv 3n-1 \mod 4\)</span>.</p>
<p>Give two solutions, following the style of the two solutions in
<a class="reference internal" href="#apply-mod-lemmas-example"><span class="std std-numref">Example 3.3.11</span></a>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">m</span> <span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">m</span> <span class="bp">&#8801;</span> <span class="n">n</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">4</span><span class="o">])</span> <span class="o">:</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">m</span> <span class="bp">-</span> <span class="mi">1</span> <span class="bp">&#8801;</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">-</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">4</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(k\)</span> be an integer, and suppose that <span class="math notranslate nohighlight">\(k\equiv 3 \mod 5\)</span>.  Show that
<span class="math notranslate nohighlight">\(4 k + k ^ 3 + 3\equiv 4 \cdot 3 + 3 ^ 3 + 3 \mod 5\)</span>.</p>
<p>Give two solutions, following the style of the two solutions in
<a class="reference internal" href="#apply-mod-lemmas-example"><span class="std std-numref">Example 3.3.11</span></a>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">k</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hb</span> <span class="o">:</span> <span class="n">k</span> <span class="bp">&#8801;</span> <span class="mi">3</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">])</span> <span class="o">:</span>
    <span class="mi">4</span> <span class="bp">*</span> <span class="n">k</span> <span class="bp">+</span> <span class="n">k</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">&#8801;</span> <span class="mi">4</span> <span class="bp">*</span> <span class="mi">3</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">+</span> <span class="mi">3</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
</ol>
</section>
</section>
<section id="modular-arithmetic-calculations">
<span id="using-modular"></span><h2><span class="section-number">3.4. </span>Modular arithmetic: calculations<a class="headerlink" href="#modular-arithmetic-calculations" title="Permalink to this headline">&#61633;</a></h2>
<section id="id33">
<h3><span class="section-number">3.4.1. </span>Example<a class="headerlink" href="#id33" title="Permalink to this headline">&#61633;</a></h3>
<p>Recall the problem from <a class="reference internal" href="#apply-mod-lemmas-example"><span class="std std-numref">Example 3.3.11</span></a>.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> be integers, and suppose that <span class="math notranslate nohighlight">\(a\equiv 2 \mod 4\)</span>.
Show that <span class="math notranslate nohighlight">\(a b ^ 2 + a ^ 2 b + 3 a \equiv 2 b ^ 2 + 2 ^ 2 \cdot b + 3 \cdot 2 \mod 4\)</span>.</p>
</div>
<p>After solving this and the many similar problems in <a class="reference internal" href="#theory-modular"><span class="std std-numref">Section 3.3</span></a>, you
probably feel like you can check the correctness of any statement of this style by sight.  And
that&#8217;s great!  When we have built up enough theory that a particular class of statement can be
checked by sight, we will stop requiring detailed proofs.  So for now on we&#8217;ll take such statements
for granted.</p>
<p>This is also usually the point at which it&#8217;s easy to write a Lean tactic which checks the
correctness of a class of statement.  I&#8217;ve done exactly this, updating tactic <code class="docutils literal notranslate"><span class="pre">rel</span></code> to cover this
kind of statement.  We won&#8217;t discuss tactic-writing in this book, but effectively, the tactic
now throws the lemmas <code class="docutils literal notranslate"><span class="pre">Int.ModEq.add</span></code>, <code class="docutils literal notranslate"><span class="pre">Int.ModEq.neg</span></code>, <code class="docutils literal notranslate"><span class="pre">Int.ModEq.sub</span></code>, <code class="docutils literal notranslate"><span class="pre">Int.ModEq.mul</span></code>,
<code class="docutils literal notranslate"><span class="pre">Int.ModEq.pow</span></code>, <code class="docutils literal notranslate"><span class="pre">Int.ModEq.refl</span></code> and the provided hypotheses at the statement until (a) the
goal is solved or (b) none of these lemmas apply any more.  And that&#8217;s exactly what we&#8217;re doing in
our heads when we check the paper statement of the problem.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">ha</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">4</span><span class="o">])</span> <span class="o">:</span>
    <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">*</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">4</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">rel</span> <span class="o">[</span><span class="n">ha</span><span class="o">]</span>
</pre></div>
</div>
</section>
<section id="id34">
<h3><span class="section-number">3.4.2. </span>Example<a class="headerlink" href="#id34" title="Permalink to this headline">&#61633;</a></h3>
<p>From now on, we will solve more interesting modular arithmetic problems, dealing with steps like
<a class="reference internal" href="#apply-mod-lemmas-example"><span class="std std-numref">Example 3.3.11</span></a> in a single line.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> be integers, with <span class="math notranslate nohighlight">\(a \equiv 4\mod 5\)</span> and
<span class="math notranslate nohighlight">\(b \equiv 3\mod 5\)</span>. Show that <span class="math notranslate nohighlight">\(ab+b^3+3 \equiv 2\mod 5\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<div class="math notranslate nohighlight">
\[\begin{split}a b + b ^ 3 + 3  &amp;\equiv 4 b + b ^ 3 + 3  \mod 5\\
&amp;\equiv 4 \cdot 3 + 3 ^ 3 + 3  \mod 5\\
&amp;=2+5 \cdot 8\\
&amp;\equiv 2\mod 5.\end{split}\]</div>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">ha</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="mi">4</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">])</span> <span class="o">(</span><span class="n">hb</span> <span class="o">:</span> <span class="n">b</span> <span class="bp">&#8801;</span> <span class="mi">3</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">])</span> <span class="o">:</span>
    <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]</span> <span class="o">:=</span>
  <span class="k">calc</span>
    <span class="n">a</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">&#8801;</span> <span class="mi">4</span> <span class="bp">*</span> <span class="n">b</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">+</span> <span class="mi">3</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">ha</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">&#8801;</span> <span class="mi">4</span> <span class="bp">*</span> <span class="mi">3</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">+</span> <span class="mi">3</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">hb</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">5</span> <span class="bp">*</span> <span class="mi">8</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">numbers</span>
    <span class="n">_</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">extra</span>
</pre></div>
</div>
</section>
<section id="id35">
<h3><span class="section-number">3.4.3. </span>Example<a class="headerlink" href="#id35" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that there exists an integer <span class="math notranslate nohighlight">\(a\)</span>, such that <span class="math notranslate nohighlight">\(6a \equiv 4\mod 11\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>The integer 8 has this property.  Indeed,</p>
<div class="math notranslate nohighlight">
\[\begin{split}6 \cdot 8 &amp;= 4 + 4 \cdot 11\\
&amp;\equiv 4\mod 11.\end{split}\]</div>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">a</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">,</span> <span class="mi">6</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="mi">4</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">11</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">use</span> <span class="mi">8</span>
  <span class="k">calc</span>
    <span class="o">(</span><span class="mi">6</span><span class="o">:</span><span class="n">&#8484;</span><span class="o">)</span> <span class="bp">*</span> <span class="mi">8</span> <span class="bp">=</span> <span class="mi">4</span> <span class="bp">+</span> <span class="mi">4</span> <span class="bp">*</span> <span class="mi">11</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">numbers</span>
    <span class="n">_</span> <span class="bp">&#8801;</span> <span class="mi">4</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">11</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">extra</span>
</pre></div>
</div>
</section>
<section id="first-mod-cases">
<span id="id36"></span><h3><span class="section-number">3.4.4. </span>Example<a class="headerlink" href="#first-mod-cases" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(x\)</span> be an integer.  Show that <span class="math notranslate nohighlight">\(x ^ 3 \equiv x\mod 3\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We consider cases according to the residue of <span class="math notranslate nohighlight">\(x\)</span> modulo 3.</p>
<p><strong>Case 1</strong> (<span class="math notranslate nohighlight">\(x\equiv 0\mod 3\)</span>):</p>
<div class="math notranslate nohighlight">
\[\begin{split}x^3 &amp;\equiv 0^3\mod 3\\
&amp; = 0\\
&amp;\equiv x\mod 3.\end{split}\]</div>
<p><strong>Case 2</strong> (<span class="math notranslate nohighlight">\(x\equiv 1\mod 3\)</span>):</p>
<div class="math notranslate nohighlight">
\[\begin{split}x^3 &amp;\equiv 1^3\mod 3\\
&amp; = 1\\
&amp;\equiv x\mod 3.\end{split}\]</div>
<p><strong>Case 3</strong> (<span class="math notranslate nohighlight">\(x\equiv 2\mod 3\)</span>):</p>
<div class="math notranslate nohighlight">
\[\begin{split}x^3 &amp;\equiv 2^3\mod 3\\
&amp; = 2 + 3 \cdot 2\\
&amp;\equiv 2\mod 3\\
&amp;\equiv x\mod 3.\end{split}\]</div>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">:</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">&#8801;</span> <span class="n">x</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">mod_cases</span> <span class="n">hx</span> <span class="o">:</span> <span class="n">x</span> <span class="bp">%</span> <span class="mi">3</span>
  <span class="k">calc</span>
    <span class="n">x</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">&#8801;</span> <span class="mi">0</span> <span class="bp">^</span> <span class="mi">3</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">hx</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">numbers</span>
    <span class="n">_</span> <span class="bp">&#8801;</span> <span class="n">x</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">hx</span><span class="o">]</span>
  <span class="k">calc</span>
    <span class="n">x</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="bp">^</span> <span class="mi">3</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">hx</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">numbers</span>
    <span class="n">_</span> <span class="bp">&#8801;</span> <span class="n">x</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">hx</span><span class="o">]</span>
  <span class="k">calc</span>
    <span class="n">x</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="bp">^</span> <span class="mi">3</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">hx</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">*</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">numbers</span>
    <span class="n">_</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">extra</span>
    <span class="n">_</span> <span class="bp">&#8801;</span> <span class="n">x</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rel</span> <span class="o">[</span><span class="n">hx</span><span class="o">]</span>
</pre></div>
</div>
</section>
<section id="id37">
<h3><span class="section-number">3.4.5. </span>Exercises<a class="headerlink" href="#id37" title="Permalink to this headline">&#61633;</a></h3>
<ol class="arabic">
<li><p>Let <span class="math notranslate nohighlight">\(n\)</span> be an integer for which <span class="math notranslate nohighlight">\(n\equiv 1\mod 3\)</span>.
Show that <span class="math notranslate nohighlight">\(n^3+7n\equiv 2\mod 3\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hn</span> <span class="o">:</span> <span class="n">n</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">])</span> <span class="o">:</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">+</span> <span class="mi">7</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">]</span> <span class="o">:=</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(a\)</span> be an integer for which <span class="math notranslate nohighlight">\(a\equiv 3\mod 4\)</span>.
Show that <span class="math notranslate nohighlight">\(a^3+4a^2+2\equiv 1\mod 4\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">ha</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="mi">3</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">4</span><span class="o">])</span> <span class="o">:</span>
    <span class="n">a</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">+</span> <span class="mi">4</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">4</span><span class="o">]</span> <span class="o">:=</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> be integers.  Show that <span class="math notranslate nohighlight">\((a + b)^3\equiv a^3+b^3\mod 3\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="o">(</span><span class="n">a</span> <span class="bp">+</span> <span class="n">b</span><span class="o">)</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">&#8801;</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">^</span> <span class="mi">3</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">3</span><span class="o">]</span> <span class="o">:=</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Show that there exists an integer <span class="math notranslate nohighlight">\(a\)</span>, such that <span class="math notranslate nohighlight">\(4a\equiv 1\mod 7\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">a</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">,</span> <span class="mi">4</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">7</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Show that there exists an integer <span class="math notranslate nohighlight">\(k\)</span>, such that <span class="math notranslate nohighlight">\(5k\equiv 6\mod 8\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">k</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">,</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">k</span> <span class="bp">&#8801;</span> <span class="mi">6</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">8</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(n\)</span> be an integer.  Show that <span class="math notranslate nohighlight">\(5n^2+3n+7\equiv 1\mod 2\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">7</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">2</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(x\)</span> be an integer.  Show that <span class="math notranslate nohighlight">\(x^5\equiv x\mod 5\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">:</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">5</span> <span class="bp">&#8801;</span> <span class="n">x</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
</ol>
</section>
</section>
<section id="bezout-s-identity">
<span id="bezout"></span><h2><span class="section-number">3.5. </span>B&#233;zout&#8217;s identity<a class="headerlink" href="#bezout-s-identity" title="Permalink to this headline">&#61633;</a></h2>
<section id="bezout-prob1">
<span id="id38"></span><h3><span class="section-number">3.5.1. </span>Example<a class="headerlink" href="#bezout-prob1" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(n\)</span> be an integer and suppose that <span class="math notranslate nohighlight">\(5n\)</span> is a multiple of <span class="math notranslate nohighlight">\(8\)</span>.  Show that
<span class="math notranslate nohighlight">\(n\)</span> is also a multiple of <span class="math notranslate nohighlight">\(8\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Since <span class="math notranslate nohighlight">\(8\mid 5n\)</span>, there exists an integer <span class="math notranslate nohighlight">\(a\)</span> such that <span class="math notranslate nohighlight">\(5n=8a\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}n &amp;= -3  (5  n) + 16 n \\
&amp;= -3  (8  a) + 16  n \\
&amp; = 8 (-3 a + 2  n),\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(8\mid n\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hn</span> <span class="o">:</span> <span class="mi">8</span> <span class="bp">&#8739;</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="mi">8</span> <span class="bp">&#8739;</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">a</span><span class="o">,</span> <span class="n">ha</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hn</span>
  <span class="n">use</span> <span class="bp">-</span><span class="mi">3</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">n</span>
  <span class="k">calc</span>
    <span class="n">n</span> <span class="bp">=</span> <span class="bp">-</span><span class="mi">3</span> <span class="bp">*</span> <span class="o">(</span><span class="mi">5</span> <span class="bp">*</span> <span class="n">n</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">16</span> <span class="bp">*</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="bp">-</span><span class="mi">3</span> <span class="bp">*</span> <span class="o">(</span><span class="mi">8</span> <span class="bp">*</span> <span class="n">a</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">16</span> <span class="bp">*</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">ha</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">8</span> <span class="bp">*</span> <span class="o">(</span><span class="bp">-</span><span class="mi">3</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">n</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
</pre></div>
</div>
<p>Such a problem will typically have many possible solutions.  Here is another solution.</p>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Since <span class="math notranslate nohighlight">\(8\mid 5n\)</span>, there exists an integer <span class="math notranslate nohighlight">\(a\)</span> such that <span class="math notranslate nohighlight">\(5n=8a\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}n &amp;= 5 (5  n) - 24 n \\
&amp;= 5  (8  a) -24  n \\
&amp; = 8 (5 a - 3  n),\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(8\mid n\)</span>.</p>
</div>
<p>Try typing the variant solution up in Lean.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hn</span> <span class="o">:</span> <span class="mi">8</span> <span class="bp">&#8739;</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="mi">8</span> <span class="bp">&#8739;</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="bezout-prob2">
<span id="id39"></span><h3><span class="section-number">3.5.2. </span>Example<a class="headerlink" href="#bezout-prob2" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that if for some integer <span class="math notranslate nohighlight">\(n\)</span> we have that <span class="math notranslate nohighlight">\(5\)</span> divides <span class="math notranslate nohighlight">\(3n\)</span>, then <span class="math notranslate nohighlight">\(5\)</span>
also divides <span class="math notranslate nohighlight">\(n\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Since <span class="math notranslate nohighlight">\(5\mid 3n\)</span>, there exists an integer <span class="math notranslate nohighlight">\(x\)</span> such that <span class="math notranslate nohighlight">\(3n=5x\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}n &amp;= 2  (3  n) - 5 n \\
&amp;= 2  (5  x) - 5  n \\
&amp; = 5 (2x -  n),\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(5\mid n\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">h1</span> <span class="o">:</span> <span class="mi">5</span> <span class="bp">&#8739;</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="mi">5</span> <span class="bp">&#8739;</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="bezout-prob3">
<span id="id40"></span><h3><span class="section-number">3.5.3. </span>Example<a class="headerlink" href="#bezout-prob3" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(m\)</span> be an integer which is divisible by 8 and by 5.  Show that it is also divisible by
40.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Since <span class="math notranslate nohighlight">\(8\mid m\)</span>, there exists an integer <span class="math notranslate nohighlight">\(a\)</span> such that <span class="math notranslate nohighlight">\(m=8a\)</span>.
Since <span class="math notranslate nohighlight">\(5\mid m\)</span>, there exists an integer <span class="math notranslate nohighlight">\(b\)</span> such that <span class="math notranslate nohighlight">\(m=5b\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}m &amp;= -15 m + 16 m\\
&amp;= -15 (8 a) + 16  m \\
&amp;= -15 (8  a) + 16  (5  b) \\
&amp; = 40 (-3  a + 2  b),\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(40\mid m\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">m</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">h1</span> <span class="o">:</span> <span class="mi">8</span> <span class="bp">&#8739;</span> <span class="n">m</span><span class="o">)</span> <span class="o">(</span><span class="n">h2</span> <span class="o">:</span> <span class="mi">5</span> <span class="bp">&#8739;</span> <span class="n">m</span><span class="o">)</span> <span class="o">:</span> <span class="mi">40</span> <span class="bp">&#8739;</span> <span class="n">m</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">a</span><span class="o">,</span> <span class="n">ha</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h1</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">b</span><span class="o">,</span> <span class="n">hb</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h2</span>
  <span class="n">use</span> <span class="bp">-</span><span class="mi">3</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span>
  <span class="k">calc</span>
    <span class="n">m</span> <span class="bp">=</span> <span class="bp">-</span><span class="mi">15</span> <span class="bp">*</span> <span class="n">m</span> <span class="bp">+</span> <span class="mi">16</span> <span class="bp">*</span> <span class="n">m</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="bp">-</span><span class="mi">15</span> <span class="bp">*</span> <span class="o">(</span><span class="mi">8</span> <span class="bp">*</span> <span class="n">a</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">16</span> <span class="bp">*</span> <span class="n">m</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">ha</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="bp">-</span><span class="mi">15</span> <span class="bp">*</span> <span class="o">(</span><span class="mi">8</span> <span class="bp">*</span> <span class="n">a</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">16</span> <span class="bp">*</span> <span class="o">(</span><span class="mi">5</span> <span class="bp">*</span> <span class="n">b</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hb</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">40</span> <span class="bp">*</span> <span class="o">(</span><span class="bp">-</span><span class="mi">3</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
</pre></div>
</div>
</section>
<section id="id41">
<h3><span class="section-number">3.5.4. </span>Exercises<a class="headerlink" href="#id41" title="Permalink to this headline">&#61633;</a></h3>
<ol class="arabic">
<li><p>Show that if 6 divides <span class="math notranslate nohighlight">\(11n\)</span>, then it divides <span class="math notranslate nohighlight">\(n\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">hn</span> <span class="o">:</span> <span class="mi">6</span> <span class="bp">&#8739;</span> <span class="mi">11</span> <span class="bp">*</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="mi">6</span> <span class="bp">&#8739;</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(a\)</span> be an integer and suppose that <span class="math notranslate nohighlight">\(5a\)</span> is a multiple of <span class="math notranslate nohighlight">\(7\)</span>.  Show that
<span class="math notranslate nohighlight">\(a\)</span> is also a multiple of <span class="math notranslate nohighlight">\(7\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">ha</span> <span class="o">:</span> <span class="mi">7</span> <span class="bp">&#8739;</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">a</span><span class="o">)</span> <span class="o">:</span> <span class="mi">7</span> <span class="bp">&#8739;</span> <span class="n">a</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Suppose that 7 and 9 are both factors of some integer <span class="math notranslate nohighlight">\(n\)</span>.  Show that 63 is also a factor of
<span class="math notranslate nohighlight">\(n\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">h1</span> <span class="o">:</span> <span class="mi">7</span> <span class="bp">&#8739;</span> <span class="n">n</span><span class="o">)</span> <span class="o">(</span><span class="n">h2</span> <span class="o">:</span> <span class="mi">9</span> <span class="bp">&#8739;</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="mi">63</span> <span class="bp">&#8739;</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(n\)</span> be an integer which is divisible by 5 and by 13.  Show that it is also divisible by
65.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">h1</span> <span class="o">:</span> <span class="mi">5</span> <span class="bp">&#8739;</span> <span class="n">n</span><span class="o">)</span> <span class="o">(</span><span class="n">h2</span> <span class="o">:</span> <span class="mi">13</span> <span class="bp">&#8739;</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="mi">65</span> <span class="bp">&#8739;</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
</ol>
</section>
</section>
</section>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="02_Proofs_with_Structure.html" class="btn btn-neutral float-left" title="2. Proofs with structure" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
        <a href="04_Proofs_with_Structure_II.html" class="btn btn-neutral float-right" title="4. Proofs with structure, II" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
    </div>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2022-2024, Heather Macbeth.  All rights reserved.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>